$\forall$$T$:Type, $L$:($T$ List), $i$:int\_seg(0; $\parallel$$L$$\parallel$). ($L$[$i$] $\in$ $L$)